h(X, Z) → f(X, s(X), Z)
f(X, Y, g(X, Y)) → h(0, g(X, Y))
g(0, Y) → 0
g(X, s(Y)) → g(X, Y)
↳ QTRS
↳ DependencyPairsProof
h(X, Z) → f(X, s(X), Z)
f(X, Y, g(X, Y)) → h(0, g(X, Y))
g(0, Y) → 0
g(X, s(Y)) → g(X, Y)
G(X, s(Y)) → G(X, Y)
H(X, Z) → F(X, s(X), Z)
F(X, Y, g(X, Y)) → H(0, g(X, Y))
h(X, Z) → f(X, s(X), Z)
f(X, Y, g(X, Y)) → h(0, g(X, Y))
g(0, Y) → 0
g(X, s(Y)) → g(X, Y)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
G(X, s(Y)) → G(X, Y)
H(X, Z) → F(X, s(X), Z)
F(X, Y, g(X, Y)) → H(0, g(X, Y))
h(X, Z) → f(X, s(X), Z)
f(X, Y, g(X, Y)) → h(0, g(X, Y))
g(0, Y) → 0
g(X, s(Y)) → g(X, Y)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
G(X, s(Y)) → G(X, Y)
h(X, Z) → f(X, s(X), Z)
f(X, Y, g(X, Y)) → h(0, g(X, Y))
g(0, Y) → 0
g(X, s(Y)) → g(X, Y)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
G(X, s(Y)) → G(X, Y)
The value of delta used in the strict ordering is 1/2.
POL(s(x1)) = 1/4 + (7/2)x_1
POL(G(x1, x2)) = (2)x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
h(X, Z) → f(X, s(X), Z)
f(X, Y, g(X, Y)) → h(0, g(X, Y))
g(0, Y) → 0
g(X, s(Y)) → g(X, Y)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
H(X, Z) → F(X, s(X), Z)
F(X, Y, g(X, Y)) → H(0, g(X, Y))
h(X, Z) → f(X, s(X), Z)
f(X, Y, g(X, Y)) → h(0, g(X, Y))
g(0, Y) → 0
g(X, s(Y)) → g(X, Y)